\begin{tabbing}
chain{-}consistent(${\it es}$;${\it Sys}$;${\it In}$;${\it isupdate}$;${\it Out}$;$f$;${\it chain}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+\+
\\[0ex]no\_repeats(Id;${\it chain}$($e$)) \& (0 $<$ $\parallel$${\it chain}$($e$)$\parallel$) \& (es{-}loc(${\it es}$; $e$) $\in$ ${\it chain}$($e$) $\in$ Id))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$), ${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]sublist(Id; (${\it chain}$($e$)); (${\it chain}$(${\it e'}$))) $\vee$ sublist(Id; (${\it chain}$(${\it e'}$)); (${\it chain}$($e$))))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex](\=($\uparrow$($e$ $\in_{b}$ ${\it In}$))\+
\\[0ex]$\Rightarrow$ (\=es{-}loc(${\it es}$; $e$)\+
\\[0ex]=
\\[0ex]if ${\it isupdate}$(${\it In}$($e$)) then hd((${\it chain}$($e$))) else last(${\it chain}$($e$)) fi 
\\[0ex]$\in$ Id))
\-\-\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ ($\neg$(es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=(adjacent(Id;${\it chain}$($e$);es{-}loc(${\it es}$; ($f$($e$)));es{-}loc(${\it es}$; $e$))\+
\\[0ex]\& adjacent(Id;${\it chain}$($f$($e$));es{-}loc(${\it es}$; ($f$($e$)));es{-}loc(${\it es}$; $e$))))
\-\-\\[0ex]\& (\=($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$)))\+
\\[0ex]$\Rightarrow$ (es{-}loc(${\it es}$; ($f$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($\forall$$a$:es{-}E{-}interface(${\it es}$;${\it Sys}$). es{-}locl(${\it es}$; $a$; $e$) $\Rightarrow$ es{-}le(${\it es}$;$a$;$f$($e$))))
\-\\[0ex]\& (($\uparrow$($e$ $\in_{b}$ ${\it Out}$)) $\Rightarrow$ (es{-}loc(${\it es}$; $e$) = last(${\it chain}$($e$)) $\in$ Id)))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$), ${\it e'}$:es{-}E{-}interface(${\it es}$;${\it Sys}$).\+
\\[0ex]es{-}locl(${\it es}$; $e$; ${\it e'}$) $\Rightarrow$ sublist(Id; (${\it chain}$(${\it e'}$)); (${\it chain}$($e$))))
\-\-
\end{tabbing}